Inference at * 1 3 1 0 2 3 1 
Iof proof for Lemma fincr wf:

.....antecedent..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
  n < (n+1) 

latex

 by ((((Arith) 
CollapseTHEN (MemCD))) 
CollapseTHEN (MemCD)) 

latex

C.

Definitions

A  B, f(a), P  Q, , a < b, s = t, n+m, x:AB(x), , {x:A| B(x)} , #$n, x:A. B(x), S  T, , t  T